NatDeq  EqDecider() 

latex

Definitions	EqDecider(T), NatDeq, nat-deq-aux, i=j, P  Q, , Prop, b, x:A. B(x), t  T
Lemmas	assert wf, iff wf, nat wf, eq int wf, nat-deq-aux